M:MsgA, a:Id. a declared in M  Prop 

latex

Definitions	MsgA, a declared in M, Prop, b, x  dom(f), KindDeq, locl(a), a:A fp B(a), x. t(x), x:A. B(x), Knd, t  T, Id
Lemmas	Id wf, Knd wf, fpf-trivial-subtype-top, locl wf, Kind-deq wf, fpf-dom wf, assert wf, msga wf